Definitions | x:A B(x), E, b, valtype(e), s = t, A & B, x:A B(x), P  Q, x:A. B(x), Msg, (x l), P & Q, state@i, ES, t T, state after e, <a,b>, Id, {T}, SQType(T), es_init(es), f(a), P  Q, P  Q, es-Trans(es), es_val(es), when-after(e;info;pred?;init;Trans;val), 2of(t), kind(e), x.A(x), let x = a in b(x), A,  b, , Prop, es-pred?(es), first(e), Unit, left+right, (state when e), val(e), Trans(i), pred(e), loc(e), s ~ t, False, kind(e), isrcv(k), islocal(k), Type, if b t else f fi, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), es_info(es), act(e), es-V(es), tag(e), lnk(e), es-M(es), es-Choose(es), acttype(e), rcvtype(e), isrcv(e), Choose(i), es-Send(es), sender(e), Send(i) |